f(s(s(s(s(s(s(s(s(x)))))))), y, y) → f(id(s(s(s(s(s(s(s(s(x))))))))), y, y)
id(s(x)) → s(id(x))
id(0) → 0
↳ QTRS
↳ DependencyPairsProof
f(s(s(s(s(s(s(s(s(x)))))))), y, y) → f(id(s(s(s(s(s(s(s(s(x))))))))), y, y)
id(s(x)) → s(id(x))
id(0) → 0
F(s(s(s(s(s(s(s(s(x)))))))), y, y) → ID(s(s(s(s(s(s(s(s(x)))))))))
ID(s(x)) → ID(x)
F(s(s(s(s(s(s(s(s(x)))))))), y, y) → F(id(s(s(s(s(s(s(s(s(x))))))))), y, y)
f(s(s(s(s(s(s(s(s(x)))))))), y, y) → f(id(s(s(s(s(s(s(s(s(x))))))))), y, y)
id(s(x)) → s(id(x))
id(0) → 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(s(s(s(s(s(s(s(s(x)))))))), y, y) → ID(s(s(s(s(s(s(s(s(x)))))))))
ID(s(x)) → ID(x)
F(s(s(s(s(s(s(s(s(x)))))))), y, y) → F(id(s(s(s(s(s(s(s(s(x))))))))), y, y)
f(s(s(s(s(s(s(s(s(x)))))))), y, y) → f(id(s(s(s(s(s(s(s(s(x))))))))), y, y)
id(s(x)) → s(id(x))
id(0) → 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
ID(s(x)) → ID(x)
f(s(s(s(s(s(s(s(s(x)))))))), y, y) → f(id(s(s(s(s(s(s(s(s(x))))))))), y, y)
id(s(x)) → s(id(x))
id(0) → 0
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ID(s(x)) → ID(x)
The value of delta used in the strict ordering is 4.
POL(ID(x1)) = (4)x_1
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
f(s(s(s(s(s(s(s(s(x)))))))), y, y) → f(id(s(s(s(s(s(s(s(s(x))))))))), y, y)
id(s(x)) → s(id(x))
id(0) → 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
F(s(s(s(s(s(s(s(s(x)))))))), y, y) → F(id(s(s(s(s(s(s(s(s(x))))))))), y, y)
f(s(s(s(s(s(s(s(s(x)))))))), y, y) → f(id(s(s(s(s(s(s(s(s(x))))))))), y, y)
id(s(x)) → s(id(x))
id(0) → 0